This paper proposes a protocol verification tool where protocols are described in an extended Petri net and Horn clauses. The extended net model contributes to reduce state space in verification with hierarchical description. The model also includes timed and colored net. Horn clause enables protocol designers to grasp a protocol by the declarative semantics. They can describe non critical but mandatory portion of a protocol like error processing or abortion with Horn clauses. Protocols are verified through simulation. Protocol verification includes two methods, all-in-one and hierarchical methods. By the all-in-one method all description is translated into Prolong clause and simulated exhaustively, whereas by the hierarchical verification, simulation begins with the lowest layer and deduces sufficient conditions that give liveness and safeness of the net model. Then the layer is replaced by a simpler net model that is incorporated into the higher layer. The scheme is applied to an illustrative example of the Alternating Bit protocol to discuss its effectiveness.

This paper proposes a hardware architecture of programmable controller based on Petri nets. The suggested architecture achieves sufficiently rapid processing even as demands on PCs become increasingly more complex. The architecture's speed and efficiency are derived from an automatic and dynamic super scalar computing capability that executes bit instructions and data handling instructions simultaneously without preprocessing, due to the properties of Petri nets. Specific characteristics for both architectural memory-based implementation of Petri nets and evolution algorithms are suggested and classified by the net structure. Analysis of the suggested architectures and effects on performance are also given with mathematical formulas and a computer simulation.

Due to the large and complex information processing systems, formal description methods are needed for specification of systems and their efficient and reliable designs. During the early stage of system design, it is often necessary to modify or change system requirements which may influence the whole system design. We have proposed a new flexible description methodology, which copes with the modifications or changes in the system requirements, in order to obtain the formal specification of the system. We have also shown that function requirements can be modeled by a Logical Petri Net (LPN), which is a kind of extended Petri Nets, in order to derive the formal specification. In this paper, we propose a verification method of system requirements that contain some kinds of logical errors. Further, we show a method to decompose and refine a requirement description hierarchically, and discuss how to derive a formal specification from a requirement description flexibly along our refinement method against the changes of the requirement description in the system.

In this paper, we discuss an abstraction method for Petri nets based on an equivalence of firing sequences of a specified subnet or a specified subset of transitions. Specifically, a method is presented to generate an equivalent net which preserves firing sequences of a specified subnet or a specified subset of transitions. The abstraction can be applied to an efficient behavioral analysis of concurrent systems constructed by composition of modules such as communication networks and Flexible Manufacturing Systems (FMS).

Rewriting logic has been proposed as a unified model of parallel and concurrent computation, especially concurrent object-oriented computation and agent oriented computation. In this paper, we present a category-theoretic technique in which simulation relation between concurrent processes described by rewriting logic is analyzed. In this technique, simulation relation is represented by morphisms in the category of concurrent processes. Moreover, this technique is shown to be applicable to Petri nets by modeling them by rewriting logic. By this method, it is acknowledged that our technique is applicable to Petri nets including multi-loops whose treatment is limited in other techniques.

Many typical control problems such as deadlock avoidance problems and mutual exclusion problems can be formulated as forbidden marking problems. This paper studies a forbidden marking problem in controlled complementary-places Petri nets, which are suitable model for sequential control systems. We show a necessary and sufficient condition for the existence of a control law for this problem. We also obtain a maximally permissive control law which allows a maximal number of transitions to fire subject to a condition that forbidden markings will never be reached.

This paper presents a novel and successful optimization algorithm for optimizing Multiple-valued Logic (MVL) functions based on Petri net theory. Mathematical properties and Petri net modeling tools to implement MVL systems are introduced. On the basis of these properties and modeling tools, the optimization algorithm can synthesize, analyze and minimize an arbitrary quaternary logic function of n-input variables. The analysis technique of optimization algorithm is a well-established concept from both theories of MVL and Petri nets, and this can be applied to specify and optimize any MVL Petri net system. In this paper, Petri nets of Galois field have been proposed in order to form a complete system, which can be used to realize and construct VLSI circuit of any MVL function. Based on the Petri nets of Galois field and the proposed algorithm, the quaternary minimum and maximum functions have been analyzed, minimized, and designed. These applications have demonstrated the usefulness of optimization algorithm. Based on Petri net theory, the analysis revealed important information about MVL Petri net modeled systems, where this information has been used to evaluate the modeled system and suggest improvements or changes. For evaluation, advantages of the proposed method over a conventional logic minimization method are presented. Also, we have observed that the MVL Petri nets have the following advantages: Designers can exhibit clearly, simply and systematically any complex MVL Petri net nodel, number of concurrent operations is increased, number of places and transitions that are needed to realize a MVL model is very small, and the interconnection problems can be greatly reduced.

In a distributed system, the protocol entities must exchange some data values and synchronization messages in order to ensure the temporal ordering of the events described in a service specification for the distributed system. It is desirable that a correct protocol specification can be derived automatically from a given service specification. In this paper, we propose an algorithm which synthesizes automatically a correct protocol specification from a service specification described as a Marked Graph with Registers (MGR) model and resources (registers and gates) allocation information. This model has a finite control modeled as a marked graph. Therefore, parallel events can be described. In our method, to minimize the number of the exchanged messages, we use a procedure to calculate an optimum solution for 0-1 integer linear programming problems. The number of the steps which each protocol entity needs to simulate one transition in the service specification is also minimized. Ways to avoiding conflict of registers are also described. Our approach has the following advantages. First, parallel events can be described in a service specification. Secondly, many practical systems can be described in the MGR model. Finally, at the protocol specification level, we can understand what events can be executed in parallel.

Nonmonotonic reasoning is a logical inference system which attempts to approximate human commonsense reasoning and is characterized as defeasible: having reasonably drawn a conclusion from some premises we may be forced to retract that conclusion upon learning new facts. This paper introduces a Petri net model for nonmonotonic reasoning with nonmonotonic rules generated by annotated logic programs and the unless operator. In the Petri net model, a fixpoint of a nonmonotonic theory can be represented as a maximal and consistent support of a firing sequence. We propose a structural method for finding extensions (coherent consequences) for a given set of nonmonotonic logic rules. It is based on the T-invariant technique for testing fireability of a goal transition in the Petri net model of Horn clause logic programs.

As to the method of multi-layer testing, up to now, the testing system (called PROVES) which testes effectively each N-layer protocol implement of SUT (System Under Test) using the functions of derail-points located between N-layer and (N+1)-layer protocol implements in a test system has been proposed. The test logic programs, which are embedded in the derail-points of the test system, play an important role to realize the protocol error test sequences in the test system. Namely, they modify, add, or delete the correct protocol commands/responses output from the protocol implement part of the lest system, sends these erroneous commands/responses to SUT and observes the output from SUT. This paper proposes the method of validating the correctness of test logic program using the structural properties of Petri nets without coding the test logic programs, where correctness means that the desired output can be obtained by sending or receiving the commands/responses within a constant time under the initial conditions determined uniquely by the test system and SUT. According to our experiment, it is seen that almost all of the logical errors included in the test logic programs used for the experiment can be detected by this method.

Net theory originated by Dr. Petri in 1962 is now indispensable key concept in the analysis and design of concurrent systems. In Japan, since late seventies the net theory has attracted attention among computer scientists. This paper reviews the historical aspect of the net theory developed in Japan during the last two decades.

This paper proposes the Total High Performance Time as a performance-related reliability measure in degradable/recoverable real-time systems. This measure reflects the effect of system behavior in pending states that are temporary states between the normal state and degraded states where the system operates in a degraded mode as a consequence of component failures. Such systems have to perform not only normal procedures but also error/recovery procedures in pending states, so the performance there is lower than that in the degraded states. In real-time systems, if performance is less than a lower limit, the response time for on-line transactions cannot meet the deadline. The consequences of failing to meet the deadline could be system failure. Therefore, the system reliability is affected significantly by whether the performance there is higher than the lower limit or not. A state where the level of performance is higher than the lower limit is called a High Performance State. We define the Total High Performance Time as the total time that the system spends operating in High Performance States. Moreover, this paper explains how to utilize the Total High Performance Time in system design. We model a method of controlling a system in pending states by using Extended Stochastic Petri Nets and obtain the characteristics necessary for evaluating the Total High Performance Time by analyzing the model. This approach is applied to a storage system that controls mirrored disks, and shown to be helpful for designing a method of controlling a system in pending states, which has been considered difficult because of the trade-off between performance and reliability.

The structural necessary and sufficient condition for "the transition-liveness means the place-liveness and vice-versa" of a subclass NII of general Petri nets is given as "the place and transition live Petri net, or PTL net, ÑII". Furthermore, "the one-token-condition Petri net, or OTC net, II" which means that every MSDL (minimal structural deadlock) is "transition and place live" under at least one initial token, i.e., II is "transition and place live" under the above initial marking. These subclasses NII, ÑII( NII), and II(ÑII) are almost the general Petri nets except at least one MSTR(minimal structural trap) and at least one pair of "a virtual MSTR or a virtual STR" and "a virtual MSDL" of an MBTR (minimal behavioral trap) in connection with making an MSDL transition-live.

Until now, in a communication system which deals with multiple processes, system behavior has been described by a fixed number of processes. The state reachability problem for specified processes was generally deliberated within a pre-defined number of processes, and was analyzed by essentially searching for all possible behaviors. However, in a system whose number of processes is arbitrary, a given state which is not reachable in some situations which consists of a small number of processes might be reachable in another situation which consists of a larger number of processes. This article discusses the above problem, assuming that the behavior of a system is described by an arbitrary number of processes. After discussing the relationship between our model and the Petri net model, we clarify the properties between the set of reachable states and the number of processes involved in the system, and show an algorithm to obtain a sufficient number of processes for resolving the reachability problem.

We describe K-NET, a support system for development of sequence control programs. The K-NET description model is based on the colored Petri net and timed Petri net. K-NET concisely expresses sequence control flow including synchronization, interlock and concurrence, and provides high-level data processing by being combined with a conventional procedural language. K-NET has an editor, simulator, generator, reporter and monitor to support the control program development procedure ranging from basic and detail design to programming and testing. We have added a new function to K-NET so it assists development of control programs for programmable controllers, and have applied it to an automatic bolt supplying system. The operation results are satisfactory.

This article discusses on PDM (Petri net based Development Methodology) which integrates approaches, modeling methods, design methods and analysis methods in a coherent manner. Although various development techniques based on Petri nets have demonstrated advantages over conventional techniques, those techniques are rather ad hoc and lack an overall picture on entire development process. PDM anticipates to provide a refernce process model to develop distributed systems with various Petri net based development methods. Behavioral properties of distrbuted systems can be an appropriate application domain of PDM.

In this paper, we show that Petri nets can be applied practically to design and analysis of concurrent, parallel and embedded mode systems such as a lift system that is familiar to our daily life. Modeling behavioral characteristics of the lift, we extend a standard Petri net by constant timed transition, faultable transition, stochastic transition and condition transition concepts. Likewise, we prsesnt some results of design and analysis of the system. This method can be applied to design and analysis of another concurrent systems.

We often use data flow diagrams or state transition diagrams to design software systems with concurrency. We call those diagrams as nets in this paper. Semantics of any methods to describe such software systems should be defined in some formal ways. There would be no doubts that any nets should be supported by appropriate theoretical frameworks. In this paper, we use CCS as a typical algebraic approach of using formulas to express concurrent behaviors and point out the different features of CCS from Petri nets. Any approaches should be not only theoretically beautiful but also practically useful. We use a specification language LOTOS as such example which has two features, CCS and ADT, and is designed to specify practical communication protocols. Algebraic approaches of using formulas, like LOTOS, can be considered as a compact way to express concurrent behaviors. We explore our discussions of net-oriented approaches into UIMS research fields. After mentioning state transition models of UIMS, we exemplify a practically used example, VIA-UIMS, which has been developed by one of authors. VIA-UIMS employs a net-oriented architecture. It has been designed to reconstuct tools which have already been widely used in many sites.

In this paper, we propose a fuzzy Petri net model for a rule-based decision making system which contains uncertain conditions and vague rules. Using the transformation method introduced in the paper, one can obtain the fuzzy Petri net of the rule-based system. Since the fuzzy Petri net can be represented by some matrices, the algebraic form of a state equation of the fuzzy Petri net is systematically derived. Both forward and backward reasoning are performed by using the state equations. Since the proposed reasoning methods require only simple arithmetic operations under a parallel rule firing scheme, it is possible to perform real-time decision making with applications to control systems and diagnostic systems. The methodology presented is also applicable to classical (nonfuzzy) knowledge base systems if the nonfuzzy system is considered as a special case of a fuzzy system with truth values being equal to the extreme values only. Finally, an illustrative example of a rule-based decision making system is given for automobile engine diagnosis.

This paper focuses on methodology underlying the application to fault tolerant computer systems with "no down communication" capability of stochastic Petri nets with general firing times. Based on a formal specification of the stochastic Petri net, we provide criteria for the marking process to be a regenerative process in continuous time with finite cycle-length moments. These results lead to strongly consistent point estimates and asymptotic confidence intervals for limiting system availability indices. We also show how the building blocks of stochastic Petri nets with general firing times facilitate the modeling of non-deterministic transition firing and illustrate the use of "interrupter input places" for graphical representation of transition interruptions.